(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 89))
(declare-fun a1 () (Array  (_ BitVec 45)  (_ BitVec 39)))
(declare-fun a2 () (Array  (_ BitVec 42)  (_ BitVec 64)))
(declare-fun a3 () (Array  (_ BitVec 126)  (_ BitVec 66)))
(assert (let ((e4(_ bv4967643992788789069434586128412165 115)))
(let ((e5 (bvmul e4 ((_ sign_extend 26) v0))))
(let ((e6 (store a2 ((_ extract 64 23) v0) ((_ extract 84 21) e5))))
(let ((e7 (select a2 ((_ extract 59 18) v0))))
(let ((e8 (select a2 ((_ extract 81 40) e5))))
(let ((e9 (select a3 ((_ sign_extend 62) e7))))
(let ((e10 (select a2 ((_ extract 44 3) v0))))
(let ((e11 (bvmul e9 e9)))
(let ((e12 (bvxor e4 ((_ sign_extend 49) e11))))
(let ((e13 (ite (= e5 ((_ zero_extend 49) e11)) (_ bv1 1) (_ bv0 1))))
(let ((e14 (ite (bvsge e7 e8) (_ bv1 1) (_ bv0 1))))
(let ((e15 ((_ extract 53 48) e10)))
(let ((e16 (bvsrem ((_ zero_extend 26) v0) e12)))
(let ((e17 (bvuge e7 e8)))
(let ((e18 (bvule e14 e14)))
(let ((e19 (distinct ((_ zero_extend 49) e11) e4)))
(let ((e20 (bvuge e5 ((_ sign_extend 51) e8))))
(let ((e21 (bvsle e8 ((_ zero_extend 58) e15))))
(let ((e22 (bvslt e12 ((_ zero_extend 26) v0))))
(let ((e23 (distinct e16 ((_ zero_extend 26) v0))))
(let ((e24 (bvslt ((_ sign_extend 25) e8) v0)))
(let ((e25 (bvsge e4 ((_ zero_extend 49) e11))))
(let ((e26 (bvslt e5 e16)))
(let ((e27 (bvule e16 ((_ zero_extend 51) e8))))
(let ((e28 (bvuge e16 e4)))
(let ((e29 (bvsgt e12 ((_ zero_extend 26) v0))))
(let ((e30 (bvslt e5 e16)))
(let ((e31 (bvsge e16 ((_ sign_extend 51) e10))))
(let ((e32 (bvsle ((_ sign_extend 26) v0) e12)))
(let ((e33 (bvsge e9 ((_ sign_extend 60) e15))))
(let ((e34 (bvsle ((_ sign_extend 60) e15) e9)))
(let ((e35 (bvsge e16 e4)))
(let ((e36 (bvsge ((_ sign_extend 49) e9) e4)))
(let ((e37 (bvsge e11 ((_ sign_extend 65) e14))))
(let ((e38 (bvugt e10 e7)))
(let ((e39 (bvuge e15 ((_ sign_extend 5) e14))))
(let ((e40 (bvsle ((_ sign_extend 51) e8) e5)))
(let ((e41 (distinct e5 ((_ sign_extend 109) e15))))
(let ((e42 (bvsge e11 e9)))
(let ((e43 (bvugt ((_ zero_extend 51) e8) e16)))
(let ((e44 (bvule ((_ sign_extend 65) e14) e11)))
(let ((e45 (bvuge ((_ zero_extend 2) e7) e9)))
(let ((e46 (bvuge e4 e12)))
(let ((e47 (bvsle ((_ zero_extend 25) e7) v0)))
(let ((e48 (bvsgt e8 e8)))
(let ((e49 (bvsgt e4 ((_ zero_extend 114) e13))))
(let ((e50 (=> e20 e41)))
(let ((e51 (ite e30 e35 e22)))
(let ((e52 (not e38)))
(let ((e53 (xor e44 e37)))
(let ((e54 (xor e46 e18)))
(let ((e55 (and e40 e52)))
(let ((e56 (xor e55 e49)))
(let ((e57 (not e36)))
(let ((e58 (and e21 e29)))
(let ((e59 (=> e24 e23)))
(let ((e60 (or e59 e34)))
(let ((e61 (or e45 e47)))
(let ((e62 (xor e39 e58)))
(let ((e63 (xor e56 e48)))
(let ((e64 (or e60 e63)))
(let ((e65 (not e51)))
(let ((e66 (ite e33 e64 e54)))
(let ((e67 (or e57 e17)))
(let ((e68 (not e67)))
(let ((e69 (and e32 e26)))
(let ((e70 (xor e62 e50)))
(let ((e71 (= e25 e31)))
(let ((e72 (or e70 e65)))
(let ((e73 (and e27 e19)))
(let ((e74 (or e42 e73)))
(let ((e75 (and e28 e43)))
(let ((e76 (ite e69 e72 e68)))
(let ((e77 (=> e66 e66)))
(let ((e78 (and e77 e61)))
(let ((e79 (or e74 e78)))
(let ((e80 (and e76 e71)))
(let ((e81 (and e80 e75)))
(let ((e82 (xor e53 e53)))
(let ((e83 (or e79 e79)))
(let ((e84 (= e82 e83)))
(let ((e85 (xor e81 e84)))
(let ((e86 (and e85 (not (= e12 (_ bv0 115))))))
(let ((e87 (and e86 (not (= e12 (bvnot (_ bv0 115)))))))
e87
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
